PR summary 87e8eb9264

Import changes for modified files

No significant changes to the import graph

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 87e8eb9).

• +0 new declarations
• −0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 87e8eb9264
Reference commit c368140668

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

!radar

Benchmark results for 87e8eb9 against c368140 are in. No significant results found. @themathqueen

• 🟥 build//instructions: +41.6G (+0.03%)

Small changes (1🟥)

• 🟥 build/module/Mathlib.Logic.Relation//instructions: +1.3G (+6.60%)

Here and in your other grind golfing PR: can you add a performance comparison (look at euprunin's PRs for an example) please? Thanks!